Inference at * 
Iof proof for Lemma exists over and r:


  T:Type, A:, B:(T). (x:T. (A  B(x)))  (A  (x:T. B(x))) 

latex

 by ((GenExRepD) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. T : Type
C1: 2. A : 
C1: 3. B : T
C1: 4. x : T
C1: 5. A
C1: 6. B(x)
C1:   x:T. B(x)
C2: 

C2: 1. T : Type
C2: 2. A : 
C2: 3. B : T
C2: 4. A
C2: 5. x : T
C2: 6. B(x)
C2:   x:T. (A  B(x))
C.

Definitions

t  T, P  Q, P  Q, x(s), P  Q, x:A. B(x), P  Q, , x:A. B(x)